1. $T$ : Type
\\[0ex]2. $x$ : $T$
\\[0ex]3. $y$ : $T$
\\[0ex]4. $u$ : $T$
\\[0ex]5. $L$ : $T$ List
\\[0ex]6. $i$ : \{0..(($\parallel$$L$$\parallel$+1) {-} 1)$^{-}$\}
\\[0ex]7. $x$ = [$u$ / $L$][$i$]
\\[0ex]8. $y$ = [$u$ / $L$][($i$+1)]
\\[0ex]9. 0 $<$ $\parallel$$L$$\parallel$
\\[0ex]10. $i$ = 0
\\[0ex]$\vdash$  ($x$ = $u$ \& $y$ = hd($L$)) $\vee$ ($\exists$$i$:\{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}. ($x$ = $L$[$i$] \& $y$ = $L$[($i$+1)]))